<html>
<head><meta charset="utf-8"><title>About the recursive solver · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html">About the recursive solver</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="222071146"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222071146" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222071146">(Jan 08 2021 at 13:22)</a>:</h4>
<p>Hey all, </p>
<p>I'm currently trying to find issues I could work on and expect to achieve anything (e.g., <a href="https://github.com/rust-lang/chalk/issues/667">chalk#667</a> was already solved when I only managed to pinpoint the problem; yet, I still learned a lot in the process, so it wasn't wasted effort). </p>
<p>Today, I've started looking into <a href="https://github.com/rust-lang/chalk/issues/587">chalk#587</a> and, while trying to figure out whether this was still relevant, I encountered some bits about the recursive solver I don't fully understand:</p>
<ul>
<li>What exactly is the purpose of the recursive solver at the moment? As far as I understood, it is supposed to be some kind of reference implementation for the SLG solver to compare against. Is that correct?</li>
<li>The recursive solver implements its own <code>Solution</code> and <code>Guidance</code> types that are nearly identical to the ones defined in chalk-solve. The only difference are some functionalities for solutions that are necessary for the recursive solver. Would it be reasonable to lift these functionalities to chalk-solve to keep the code DRY? Or would it be better to make the recursive solution a newtype for the general solution?</li>
<li>What is the correct way to translate test cases from the SLG solver to the recursive solver? E.g., if the test case tests <code>yields_first[SolverChoice::slg(2, None)</code> and expects an ambiguous substitution result, would this correspond to testing <code>yields[SolverChoice::recursive(2,100)</code> expecting an ambiguous solution with the same substitution? And should a floundered result correspond to an ambiguous solution with no inference guidance, etc.?</li>
</ul>
<p>I'm really sorry, if this is a bit much to answer at once. Though, every little guidance would help me understanding a bit more.</p>



<a name="222078092"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222078092" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222078092">(Jan 08 2021 at 14:29)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/About.20the.20recursive.20solver/near/222071146">said</a>:</p>
<blockquote>
<p><a href="https://github.com/rust-lang/chalk/issues/667">chalk#667</a> was already solved when I only managed to pinpoint the problem; yet, I still learned a lot in the process, so it wasn't wasted effort</p>
</blockquote>
<p>Oops, sorry to snipe you <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span> I'm glad you feel like your learned something in the process. I would be happy to discuss the problem/solution with you if you think that'll help too.</p>



<a name="222078168"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222078168" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222078168">(Jan 08 2021 at 14:30)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/About.20the.20recursive.20solver/near/222071146">said</a>:</p>
<blockquote>
<ul>
<li>What exactly is the purpose of the recursive solver at the moment? As far as I understood, it is supposed to be some kind of reference implementation for the SLG solver to compare against. Is that correct?<br>
I'm really sorry, if this is a bit much to answer at once. Though, every little guidance would help me understanding a bit more.</li>
</ul>
</blockquote>
<p>So, the recursive solver is essentially a <em>different</em> PROLOG-ish trait solver implementation.</p>



<a name="222078279"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222078279" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222078279">(Jan 08 2021 at 14:31)</a>:</h4>
<p>So, let's think about the crates:</p>



<a name="222078363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222078363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222078363">(Jan 08 2021 at 14:31)</a>:</h4>
<p><code>chalk-ir</code> essentially defines the types of Rust, and the goals we can use to solve questions about these types</p>



<a name="222078540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222078540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222078540">(Jan 08 2021 at 14:32)</a>:</h4>
<p><code>chalk-solve</code> defines the rules for how these types interact and defines an interface for allowing impls, traits, structs, etc. to be defined</p>



<a name="222079200"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222079200" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222079200">(Jan 08 2021 at 14:38)</a>:</h4>
<p><code>chalk-engine</code> is a solver implementation based around the SLG algorithm. The core idea behind is that each canonical goal (e.g. <code>for&lt;T&gt; Implemented(Foo&lt;T&gt;: Bar)</code>) has it's own <code>Table</code>. There may be multiple ways to solve this goal, each represented by a <code>Strand</code>. Because there may be multiple ways to solve the goal, there may be multiple (or infinite) answers. (e.g. <code>T = u32</code>, <code>T = i32</code>). Then, to get a final answer, you have to aggregate them to find a general solution.</p>



<a name="222079666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222079666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222079666">(Jan 08 2021 at 14:43)</a>:</h4>
<p><code>chalk-recursive</code> is a solver implementation that to my knowledge is roughly based around the current rustc implementation. The core idea being that rather than each canonical goal being solved independently, you always keep around the "current state" of the solution. I don't have an example off the top of my head, but I think there are some examples in the book (if not, message me later an we can discuss)</p>



<a name="222080193"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222080193" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222080193">(Jan 08 2021 at 14:48)</a>:</h4>
<p>We currrently don't know between <code>chalk-engine</code> and <code>chalk-recursive</code> which is better. First, <code>chalk-engine</code> has a big problem w.r.t. associated types (<a href="https://github.com/rust-lang/chalk/issues/234">chalk#234</a>). But <code>chalk-recursive</code> has some problems when solving WF goals (<a href="https://github.com/rust-lang/chalk/issues/587">chalk#587</a>; this might not be chalk-recursive's fault, it could be in the WF rules). We also aren't sure how performance will differ between the two once all the obvious/relevant optimizations are done. Theoretically, SLG answers are more "reusable", but e.g. rust-analyzer was always throwing away those between solves because of memory. Also, theoretically, the SLG is more "complete" (example in book), but even the current rustc implementation can't solve that example.</p>



<a name="222080533"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222080533" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222080533">(Jan 08 2021 at 14:51)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/About.20the.20recursive.20solver/near/222071146">said</a>:</p>
<blockquote>
<ul>
<li>The recursive solver implements its own <code>Solution</code> and <code>Guidance</code> types that are nearly identical to the ones defined in chalk-solve. The only difference are some functionalities for solutions that are necessary for the recursive solver. Would it be reasonable to lift these functionalities to chalk-solve to keep the code DRY? Or would it be better to make the recursive solution a newtype for the general solution?</li>
</ul>
</blockquote>
<p>Completely reasonable to move code around to deduplicate things :) There's been some refactoring/moving around in terms of crates that I don't remember if there's still a reason these types are in chalk-recursive or not. At one point, chalk-solve depended on chalk-engine and chalk-recursive, so the types had to be duplicated between the two. But not, idk. If there's some refactoring you can find to make things cleaner, by all means PR them :)</p>



<a name="222081164"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222081164" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222081164">(Jan 08 2021 at 14:56)</a>:</h4>
<p>First of all, already a big thanks for the really detailed answers.</p>
<blockquote>
<p>We currrently don't know between chalk-engine and chalk-recursive which is better.</p>
</blockquote>
<p>Ah ok, so it's still undecided/undecidable . That was in fact the part that I didn't catch before.</p>
<blockquote>
<p>by all means PR them :)</p>
</blockquote>
<p>On it, I just wanted to get a clearer picture  of these things first. <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span></p>



<a name="222081174"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222081174" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222081174">(Jan 08 2021 at 14:56)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/About.20the.20recursive.20solver/near/222071146">said</a>:</p>
<blockquote>
<ul>
<li>What is the correct way to translate test cases from the SLG solver to the recursive solver? E.g., if the test case tests <code>yields_first[SolverChoice::slg(2, None)</code> and expects an ambiguous substitution result, would this correspond to testing <code>yields[SolverChoice::recursive(2,100)</code> expecting an ambiguous solution with the same substitution? And should a floundered result correspond to an ambiguous solution with no inference guidance, etc.?</li>
</ul>
</blockquote>
<p>So, there's not <em>exactly</em> a 1:1 translation between <code>yields_first[SolverChoice::slg(2, None)</code> and <code>yields[SolverChoice::recursive(2,100)</code>. The closest would be <code>yields[SolverChoice::recursive(N,2)</code> or something. I think it depends on what the test is supposed to be tested in terms of what the choice is. <code>yields_first</code> isn't a complete answer. It's only <code>T = u32</code> from the example a bit above, not the general <code>T = ?0</code>. The recursive solver doesn't know anything about this.</p>



<a name="222081251"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222081251" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222081251">(Jan 08 2021 at 14:57)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/About.20the.20recursive.20solver/near/222071146">said</a>:</p>
<blockquote>
<p>I'm really sorry, if this is a bit much to answer at once. Though, every little guidance would help me understanding a bit more.</p>
</blockquote>
<p>No reason to be sorry. I'm quite happy to help answer things. Let me know if I missed anything or I need to clarify</p>



<a name="222085535"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222085535" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222085535">(Jan 08 2021 at 15:31)</a>:</h4>
<blockquote>
<p>rust-analyzer was always throwing away those between solves because of memory</p>
</blockquote>
<p>hmm actually I think we stopped reusing the solver because it made it impossible to accurately track dependencies for each trait query, hence making it impossible to reuse solutions <em>across edits</em></p>



<a name="222085998"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222085998" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222085998">(Jan 08 2021 at 15:35)</a>:</h4>
<p>(also, reusing the solver was complicated wrt panic and thread safety)</p>



<a name="222086510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222086510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222086510">(Jan 08 2021 at 15:39)</a>:</h4>
<p>So, as far as I understand rust-analyzer uses the SLG solver primarily, yet does not reuse it as it is meant to be. Does rust-analyzer make use of the recursive solver in the current stable release as well? And if so, which of those two fits the use case of rust-analyzer better?</p>



<a name="222086723"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222086723" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222086723">(Jan 08 2021 at 15:41)</a>:</h4>
<p>no, rust-analyzer uses the recursive solver, mainly because of <a href="https://github.com/rust-lang/chalk/issues/234">chalk#234</a></p>



<a name="222087105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222087105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222087105">(Jan 08 2021 at 15:45)</a>:</h4>
<p>the recursive solver was primarily resurrected to solve that bug; before that, we used the SLG solver</p>



<a name="222087256"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222087256" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222087256">(Jan 08 2021 at 15:46)</a>:</h4>
<p>I see, that makes sense. Thanks for the clarification. Such past decisions are sometimes a bit hard to track down <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span></p>



<a name="222883199"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222883199" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222883199">(Jan 15 2021 at 16:28)</a>:</h4>
<p>As a bit of a follow up to the previous discussion, I looked further into <a href="https://github.com/rust-lang/chalk/issues/587">chalk#587</a> and would like to discuss some results.<br>
Of the tests mentioned in <a href="https://github.com/rust-lang/chalk/issues/587">chalk#587</a> only two are reproducibly problematic with the recursive solver in regard to WF checking: <code>wf_lowering::ill_formed_type_in_header</code> and <code>wf_lowering::higher_ranked_cyclic_requirements</code></p>
<p>So far I only looked into the first one in greater detail. It became apparent that it fails with a stack overflow due to the recursive solver's eager search for more solutions. For the goal <code>WellFormed(!1_0: Bar)</code> both the SLG and the recursive solver find the same unique solution from the environment. Yet, only the recursive solver tries additionally an (seemingly) endless loop of <code>AliasEq(&lt;(Foo::Value)&lt;!1_0&gt; as Foo&gt;::Value = ^0.0)</code> (and similar goals) where <code>!1_0</code> only gets exchanged for ever more instances of the placeholder <code>(Foo::Value)&lt;!1_0&gt;</code> like so:</p>
<div class="codehilite"><pre><span></span><code>AliasEq(&lt;(Foo::Value)&lt;(Foo::Value)&lt;(Foo::Value)&lt;....&lt;!1_0&gt;...&gt;&gt;&gt; as Foo&gt;::Value = ^0.0)
</code></pre></div>
<p>There are at least two possible solutions to this and I would love to hear some opinions on them:</p>
<ul>
<li>We could prohibit such recursively growing goals by some kind of heuristic. Yet, I'm not sure whether this behaviour of nesting associated type placeholders would actually be necessary to solve some special cases or if it would be feasible to simply prohibit them. Just from the sound of it, nested associated type placeholders seem a bit odd.</li>
<li>Fortunately, the goals are only getting bigger. Therefore, the recursive solver is able to cancel computations before the stack overflows if it is not invoked with the default maximum goal size (e.g. 25 instead of 30 does the trick). Changing <code>recursive_default()</code> to use a maximum goal size of 25 would not change any other test results, though such a simple workaround seems to miss the core of the problem.</li>
</ul>



<a name="222888016"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222888016" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222888016">(Jan 15 2021 at 16:56)</a>:</h4>
<p>I have to think more about this, but it's weird to me that its hitting an infinite loop instead of being caught as getting to big and being ambiguous (i.e. needs truncation)</p>



<a name="222888143"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222888143" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222888143">(Jan 15 2021 at 16:56)</a>:</h4>
<p>Also, I'm assuming that isn't a problem in SLG because of <a href="https://github.com/rust-lang/chalk/issues/234">chalk#234</a>?</p>



<a name="222888585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222888585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222888585">(Jan 15 2021 at 16:59)</a>:</h4>
<p>Yes, the SLG solver does not run into this problem. It also less of an infinite loop and more of a rather slowly growing formula. The truncation does help, but not for a maximum size of 30.</p>



<a name="222889179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222889179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222889179">(Jan 15 2021 at 17:03)</a>:</h4>
<p>On an other note, <span class="user-mention" data-user-id="232957">@Jack Huey</span> you were the last one to update the status of <a href="https://github.com/rust-lang/chalk/issues/587">chalk#587</a> . You seem to have checked both <code>test::misc::subgoal_cycle_inhabited</code> and <code>test::misc::subgoal_cycle_uninhabited</code> with the recursive solver. May I ask what goals you used for these tests? Both use <code>yields_first</code> and I'm a bit lost at how to transform these goals for the recursive solver.</p>



<a name="222890566"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222890566" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222890566">(Jan 15 2021 at 17:11)</a>:</h4>
<p>I mean, that sounds like an infinite loop though? <code>1_0</code> will always turn into <code>(Foo::Value)&lt;!1_0&gt;</code>, so it will always loop. What do you mean truncation doesn't help at 30? Does it stop then somehow?</p>



<a name="222890636"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222890636" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222890636">(Jan 15 2021 at 17:11)</a>:</h4>
<p>And for the tests, I changed the solver for WF checking to SLG in test/mod</p>



<a name="222891210"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222891210" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222891210">(Jan 15 2021 at 17:15)</a>:</h4>
<p>For a maximum size of 30 (as in the default settings for the recursive solver) the test will run into an stack overflow as the goals are growing slower than the call stack. If truncation already stops computation at goals of, for example, size 25, than the stack overflow doesn't happen but the correct result is achieved.</p>



<a name="222902628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/About%20the%20recursive%20solver/near/222902628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/About.20the.20recursive.20solver.html#222902628">(Jan 15 2021 at 18:29)</a>:</h4>
<p>Sounds like we need something like stacker for the recursive solver</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>